This is an experimental branch that does the following:

• Introduces a new pass, "subdep" that combines "sub" and "sub expansion" with the "sub expansion" step made even bigger by expanding relation rules, type cases, and function clauses whenever there is a sub type expression present in a type family's arguments. This allows the validation to be able to reduce these type families and show that they are in fact equivalent.
• Fix on the evaluator that was removing CvtE whenever it failed to convert a numtyp to another.
• Fix on sub pass that did not preserve dependent types correctly in projection functions.
• Fix on improveids in order to aid the evaluator when modifying the environment per definition.

Currently a draft until we figure out testing in this case.